T:Type. 
subtype_rel(T; )
 (x:T, L:(T List). sorted(L)  no_repeats(T; L)  no_repeats(T; s-insert(x; L))) 

latex

Definitions

x:A. B(x), P  Q, no_repeats(T; l), sorted(L), t  T, s-insert(x; l), A, prop{i:l}, , A  B, l[i], int_seg(i; j), ||as||, (i = j), Unit, T, i <z j, , b, b, i z j, True, P  Q, P  Q, P  Q, False, (x  l), P  Q, l_all(L; T; x.P(x))

Lemmas

member-s-insert, cons member, l member wf, sorted-cons, s-insert wf, no repeats cons, le int wf, assert wf, bnot wf, bool wf, lt int wf, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, iff transitivity, assert of lt int, eqtt to assert, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, sorted wf, no repeats wf, length wf2, select wf, le wf, int seg wf, not wf, nat wf